Multi-objective verification problems of parametric Markov decision processesunder optimality criteria can be naturally expressed as nonlinear programs. Weobserve that many of these computationally demanding problems belong to thesubclass of signomial programs. This insight allows for a sequentialoptimization algorithm to efficiently compute sound but possibly suboptimalsolutions. Each stage of this algorithm solves a geometric programming problem.These geometric programs are obtained by convexifying the nonconvex constraintsof the original problem. Direct applications of the encodings as nonlinear pro-grams are model repair and parameter synthesis. We demonstrate the scalabilityand quality of our approach by well-known benchmarks
展开▼
